Search Results

Documents authored by Cockx, Jesper

Document
DOI: 10.4230/OASIcs.EVCS.2023.6
Dependently Typed Languages in Statix

Authors: Jonathan Brouwer, Jesper Cockx, and Aron Zwaan

Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)

Abstract
Static type systems can greatly enhance the quality of programs, but implementing a type checker that is both expressive and user-friendly is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of a type system. However, so far Statix has not been used to implement dependent types, which is a class of type systems which require evaluation of terms during type checking. In this paper, we present an implementation of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types.
Cite as

Jonathan Brouwer, Jesper Cockx, and Aron Zwaan. Dependently Typed Languages in Statix. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{brouwer_et_al:OASIcs.EVCS.2023.6,
  author =	{Brouwer, Jonathan and Cockx, Jesper and Zwaan, Aron},
  title =	{{Dependently Typed Languages in Statix}},
  booktitle =	{Eelco Visser Commemorative Symposium (EVCS 2023)},
  pages =	{6:1--6:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-267-9},
  ISSN =	{2190-6807},
  year =	{2023},
  volume =	{109},
  editor =	{L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.6},
  URN =		{urn:nbn:de:0030-drops-177769},
  doi =		{10.4230/OASIcs.EVCS.2023.6},
  annote =	{Keywords: Spoofax, Statix, Dependent Types, Scope Graphs, Calculus of Constructions}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.TYPES.2021
LIPIcs, Volume 239, TYPES 2021, Complete Volume

Authors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
LIPIcs, Volume 239, TYPES 2021, Complete Volume
Cite as

27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 1-280, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{basold_et_al:LIPIcs.TYPES.2021,
  title =	{{LIPIcs, Volume 239, TYPES 2021, Complete Volume}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{1--280},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021},
  URN =		{urn:nbn:de:0030-drops-167680},
  doi =		{10.4230/LIPIcs.TYPES.2021},
  annote =	{Keywords: LIPIcs, Volume 239, TYPES 2021, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.TYPES.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Henning Basold, Jesper Cockx, and Silvia Ghilezan

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 0:i-0:viii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{basold_et_al:LIPIcs.TYPES.2021.0,
  author =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{0:i--0:viii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.0},
  URN =		{urn:nbn:de:0030-drops-167691},
  doi =		{10.4230/LIPIcs.TYPES.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2019.2
Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules

Authors: Jesper Cockx

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)

Abstract
Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes - such as strictly positive datatypes, complete case analysis, and well-founded induction - that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as η-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: yours.
Cite as

Jesper Cockx. Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 2:1-2:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cockx:LIPIcs.TYPES.2019.2,
  author =	{Cockx, Jesper},
  title =	{{Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{2:1--2:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.2},
  URN =		{urn:nbn:de:0030-drops-130666},
  doi =		{10.4230/LIPIcs.TYPES.2019.2},
  annote =	{Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact